M1, M2, M:MsgA. M1 || M2  M  M2  M  M1  M2 

latex

Definitions	P & Q, M1  M2, M1  M2, M1 || M2, MsgA, t  T, x:A. B(x), P  Q, M1 ||decl M2
Lemmas	ma-join wf, ma-sub transitivity, ma-sub-join-right, msga wf, ma-compatible wf, ma-sub wf